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

proof

let a, b be Function of Y,BOOLEAN; :: thesis: ( a '<' b implies a 'imp' b = I_el Y )
assume A2: a '<' b ; :: thesis: a 'imp' b = I_el Y
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 . x = FALSE & b . x = FALSE ) or ( a . x = FALSE & b . x = TRUE ) or ( a . x = TRUE & b . x = TRUE ) ) by A2, XBOOLEAN:def 3;
hence ('not' (a . x)) 'or' (b . x) = TRUE ; :: thesis: verum

end;

let x be Element of Y; :: according to FUNCT_2:def 8 :: 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 Def8, Def11;
hence (a 'imp' b) . x = (I_el Y) . x by A3; :: thesis: verum

end;

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

proof

let a, b be Function of Y,BOOLEAN; :: thesis: ( a 'imp' b = I_el Y implies a '<' b )
assume A4: a 'imp' b = I_el Y ; :: thesis: a '<' b
A5: 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 Def8;
hence ('not' (a . x)) 'or' (b . x) = TRUE by A4, Def11; :: 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 ) )
A6: ( ( '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 A5;
hence ( ( a . x = FALSE & b . x = FALSE ) or ( a . x = FALSE & b . x = TRUE ) or ( a . x = TRUE & b . x = TRUE ) ) by A6; :: thesis: verum

end;

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

end;

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