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 '<' 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 )
consider k3 being Function such that
A2: a 'imp' b = k3 and
A3: dom k3 = Y and
rng k3 c= BOOLEAN by FUNCT_2:def 2;
consider k4 being Function such that
A4: I_el Y = k4 and
A5: dom k4 = Y and
rng k4 c= BOOLEAN by FUNCT_2:def 2;
assume A6: a '<' b ; :: thesis: a 'imp' b = I_el Y
A7: 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 A6, 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;

A8: 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 A7;
hence ('not' (a . x)) 'or' (b . x) = TRUE ; :: thesis: verum

end;

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
( (a 'imp' b) . x = ('not' (a . x)) 'or' (b . x) & (I_el Y) . x = TRUE ) by Def11, Def14;
hence (a 'imp' b) . x = (I_el Y) . x by A8; :: thesis: verum

end;

then for u being set st u in Y holds
k3 . u = k4 . u by A2, A4;
hence a 'imp' b = I_el Y by A2, A3, A4, A5, FUNCT_1:9; :: thesis: verum

end;

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 A9: a 'imp' b = I_el Y ; :: thesis: a '<' b
A10: 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 A9, 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 ) )
A11: ( ( '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 A10;
hence ( ( a . x = FALSE & b . x = FALSE ) or ( a . x = FALSE & b . x = TRUE ) or ( a . x = TRUE & b . x = TRUE ) ) by A11; :: 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;

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