let X be StackAlgebra; :: thesis: for s being stack of X st emp s holds
Class ((==_ X),s) = the s_empty of X
let s be stack of X; :: thesis: ( emp s implies Class ((==_ X),s) = the s_empty of X )
assume A1: emp s ; :: thesis: Class ((==_ X),s) = the s_empty of X
thus Class ((==_ X),s) c= the s_empty of X :: according to XBOOLE_0:def 10 :: thesis: the s_empty of X c= Class ((==_ X),s)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Class ((==_ X),s) or x in the s_empty of X )
assume A2: x in Class ((==_ X),s) ; :: thesis: x in the s_empty of X
then reconsider s1 = x as stack of X ;
[s,s1] in ==_ X by A2, EQREL_1:18;
then s == s1 by Def16;
then emp s1 by A1, Th14;
hence x in the s_empty of X ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the s_empty of X or x in Class ((==_ X),s) )
assume A3: x in the s_empty of X ; :: thesis: x in Class ((==_ X),s)
then reconsider s1 = x as stack of X ;
emp s1 by A3;
then s == s1 by A1, Th15;
then [s,s1] in ==_ X by Def16;
hence x in Class ((==_ X),s) by EQREL_1:18; :: thesis: verum