let Y be non empty set ; :: thesis: for a, b being Element of Funcs Y,BOOLEAN holds
( a 'imp' b = I_el Y iff a '<' b )
let a, b be Element of Funcs Y,BOOLEAN ; :: thesis: ( a 'imp' b = I_el Y iff a '<' b )
A1: for a, b being Element of Funcs Y,BOOLEAN st a 'imp' b = I_el Y holds
a '<' b

proof

let a, b be Element of Funcs Y,BOOLEAN ; :: thesis: ( a 'imp' b = I_el Y implies a '<' b )
assume A2: a 'imp' b = I_el Y ; :: thesis: a '<' b
A3: for x being Element of Y holds ('not' (a . x)) 'or' (b . x) = TRUE

proof

let x be Element of Y; :: thesis: ('not' (a . x)) 'or' (b . x) = TRUE
(a 'imp' b) . x = ('not' (a . x)) 'or' (b . x) by Def11;
hence ('not' (a . x)) 'or' (b . x) = TRUE by A2, Def14; :: thesis: verum

end;

for x being Element of Y holds
( ( a . x = FALSE & b . x = FALSE ) or ( a . x = FALSE & b . x = TRUE ) or ( a . x = TRUE & b . x = TRUE ) )

proof

let x be Element of Y; :: thesis: ( ( a . x = FALSE & b . x = FALSE ) or ( a . x = FALSE & b . x = TRUE ) or ( a . x = TRUE & b . x = TRUE ) )
A4: ( ( 'not' (a . x) = TRUE & b . x = FALSE ) or ( 'not' (a . x) = TRUE & b . x = TRUE ) or ( 'not' (a . x) = FALSE & b . x = FALSE ) or ( 'not' (a . x) = FALSE & b . x = TRUE ) ) by XBOOLEAN:def 3;
('not' (a . x)) 'or' (b . x) = TRUE by A3;
hence ( ( a . x = FALSE & b . x = FALSE ) or ( a . x = FALSE & b . x = TRUE ) or ( a . x = TRUE & b . x = TRUE ) ) by A4; :: thesis: verum

end;

then for x being Element of Y st a . x = TRUE holds
b . x = TRUE ;
hence a '<' b by Def15; :: thesis: verum

end;

for a, b being Element of Funcs Y,BOOLEAN st a '<' b holds
a 'imp' b = I_el Y

proof

let a, b be Element of Funcs Y,BOOLEAN ; :: thesis: ( a '<' b implies a 'imp' b = I_el Y )
assume A5: a '<' b ; :: thesis: a 'imp' b = I_el Y
A6: for x being Element of Y holds
( ( a . x = FALSE & b . x = FALSE ) or ( a . x = FALSE & b . x = TRUE ) or ( a . x = TRUE & b . x = TRUE ) )

proof

let x be Element of Y; :: thesis: ( ( a . x = FALSE & b . x = FALSE ) or ( a . x = FALSE & b . x = TRUE ) or ( a . x = TRUE & b . x = TRUE ) )
( a . x = TRUE implies b . x = TRUE ) by A5, Def15;
hence ( ( a . x = FALSE & b . x = FALSE ) or ( a . x = FALSE & b . x = TRUE ) or ( a . x = TRUE & b . x = TRUE ) ) by XBOOLEAN:def 3; :: thesis: verum

end;

A7: for x being Element of Y holds ('not' (a . x)) 'or' (b . x) = TRUE

proof

let x be Element of Y; :: thesis: ('not' (a . x)) 'or' (b . x) = TRUE
( ( a . x = FALSE & b . x = FALSE ) or ( a . x = FALSE & b . x = TRUE ) or ( a . x = TRUE & b . x = TRUE ) ) by A6;
hence ('not' (a . x)) 'or' (b . x) = TRUE ; :: thesis: verum

end;

A8: for x being Element of Y holds (a 'imp' b) . x = (I_el Y) . x

proof

let x be Element of Y; :: thesis: (a 'imp' b) . x = (I_el Y) . x
A9: (a 'imp' b) . x = ('not' (a . x)) 'or' (b . x) by Def11;
(I_el Y) . x = TRUE by Def14;
hence (a 'imp' b) . x = (I_el Y) . x by A7, A9; :: thesis: verum

end;

consider k3 being Function such that
A10: ( a 'imp' b = k3 & dom k3 = Y & rng k3 c= BOOLEAN ) by FUNCT_2:def 2;
consider k4 being Function such that
A11: ( I_el Y = k4 & dom k4 = Y & rng k4 c= BOOLEAN ) by FUNCT_2:def 2;
for u being set st u in Y holds
k3 . u = k4 . u by A8, A10, A11;
hence a 'imp' b = I_el Y by A10, A11, FUNCT_1:9; :: thesis: verum

end;

hence ( a 'imp' b = I_el Y iff a '<' b ) by A1; :: thesis: verum